feat(MerkleTree): add tweaked Merkle authentication paths with completeness and tweak-tagged collision binding - #474

VCVio/CryptoFoundations/MerkleTree/Addressed/Basic.lean (19)

• def AddressedCollision {s : Skeleton} (nodeHash : NodeAddress s → α → α → α)
• def addressedNodeHash {PkSeed Tweak Y : Type} (th : TweakableHash PkSeed Tweak (Y × Y) Y)
• def buildMerkleTreeAddressedWithHash {s : Skeleton} (leaf_tree : LeafData α s)
• def childPairAt : {s : Skeleton} → FullData α s → NodeAddress s → α × α
• def findCollisionAddressed : {s : Skeleton} → (nodeHash : NodeAddress s → α → α → α) →
• def getPutativeRootAddressedWithHash :
• def levelNodeHash {PkSeed Tweak Y : Type} (th : TweakableHash PkSeed Tweak (Y × Y) Y)
• def pathDepth : {s : Skeleton} → NodeAddress s → ℕ
• def populateUpAddressed : {s : Skeleton} → (nodeHash : NodeAddress s → α → α → α) →
• def subtreeDepth : {s : Skeleton} → NodeAddress s → ℕ
• theorem addressed_functional_completeness {s : Skeleton}
• theorem addressed_oriented_binding {s : Skeleton}
• theorem findCollisionAddressed_isSome {s : Skeleton}
• theorem findCollisionAddressed_oriented {s : Skeleton}
• theorem findCollisionAddressed_sound {s : Skeleton}
• theorem getPutativeRootAddressedWithHash_binding_collision {s : Skeleton}
• theorem getPutativeRootAddressed_const (h : α → α → α) {s : Skeleton}
• theorem levelNodeHash_eq_addressed {PkSeed Tweak Y : Type}
• theorem populateUpAddressed_const (h : α → α → α) {s : Skeleton}

VCVio/CryptoFoundations/MerkleTree/Addressed/Level.lean (4)

• def buildMerkleTreeLevel (th : TweakableHash PkSeed Tweak (Y × Y) Y) (pk : PkSeed)
• def getPutativeRootLevel (th : TweakableHash PkSeed Tweak (Y × Y) Y) (pk : PkSeed)
• theorem level_functional_completeness (th : TweakableHash PkSeed Tweak (Y × Y) Y)
• theorem level_oriented_binding (th : TweakableHash PkSeed Tweak (Y × Y) Y)

• VCVio.lean: Added imports for two new modules, VCVio.CryptoFoundations.MerkleTree.Addressed.Basic and VCVio.CryptoFoundations.MerkleTree.Addressed.Level, which bring in definitions and results related to an addressed variant of the Merkle tree structure.
• VCVio/CryptoFoundations/MerkleTree/Addressed/Basic.lean: This new file defines the AddressedMerkleTree namespace, implementing a generic engine for Merkle trees whose node hash depends on the node's full typed address (NodeAddress s). It introduces the inductive type NodeAddress for paths to internal nodes, along with the core constructions populateUpAddressed/buildMerkleTreeAddressedWithHash (cache building) and getPutativeRootAddressedWithHash (root recomputation). The theorem addressed_functional_completeness proves that honest authentication paths verify correctly for any address-dependent hash. The kernel findCollisionAddressed produces an address-tagged collision when two openings agree on the root but differ in leaf value or path, with soundness and isSome guarantees (findCollisionAddressed_sound, findCollisionAddressed_isSome); getPutativeRootAddressedWithHash_binding_collision packages this as a user-facing binding statement. Two oriented theorems (findCollisionAddressed_oriented, addressed_oriented_binding) refine the collision to expose the honestly-precommitted child pair at the tagged address, suitable for a target-collision reduction. Finally, instances show that constant nodeHash recovers the unaddressed engine (getPutativeRootAddressed_const, populateUpAddressed_const), and the file provides levelNodeHash (via subtreeDepth) and addressedNodeHash (via an arbitrary map) to instantiate level-separated and fully-addressed (XMSS-style) trees, with levelNodeHash_eq_addressed showing the former factor through the latter.
• VCVio/CryptoFoundations/MerkleTree/Addressed/Level.lean: This new file Level.lean introduces a level-separated (per-subtree-depth) specialization of the addressed Merkle tree engine. It defines buildMerkleTreeLevel and getPutativeRootLevel that wrap the generic buildMerkleTreeAddressedWithHash and getPutativeRootAddressedWithHash with levelNodeHash. Two theorems from the engine are instantiated: level_functional_completeness (verifying that a generated proof recovers the root) and level_oriented_binding (establishing an oriented collision-binding property under the tweak of the collision's level). No sorry or admit appear in the file.

ToMathlib/Data/IndexedBinaryTree/Basic.lean (1)

• def SkeletonInternalIndex.subtreeDepth :

VCVio/CryptoFoundations/MerkleTree/Addressed/Basic.lean (20)

• def AddressedCollision {s : Skeleton} (nodeHash : SkeletonInternalIndex s → α → α → α)
• def addressedNodeHash {PkSeed Tweak Y : Type} (th : TweakableHash PkSeed Tweak (Y × Y) Y)
• def buildMerkleTreeAddressedWithHash {s : Skeleton} (leaf_tree : LeafData α s)
• def childPairAt : {s : Skeleton} → FullData α s → SkeletonInternalIndex s → α × α
• def findCollisionAddressed : {s : Skeleton} → (nodeHash : SkeletonInternalIndex s → α → α → α) →
• def getPutativeRootAddressedWithHash :
• def levelNodeHash {PkSeed Tweak Y : Type} (th : TweakableHash PkSeed Tweak (Y × Y) Y)
• def populateUpAddressed : {s : Skeleton} → (nodeHash : SkeletonInternalIndex s → α → α → α) →
• theorem addressed_functional_completeness {s : Skeleton}
• theorem addressed_oriented_binding {s : Skeleton}
• theorem buildMerkleTreeAddressed_const (h : α → α → α) {s : Skeleton}
• theorem findCollisionAddressed_const (h : α → α → α) {s : Skeleton}
• theorem findCollisionAddressed_isSome {s : Skeleton}
• theorem findCollisionAddressed_oriented {s : Skeleton}
• theorem findCollisionAddressed_sound {s : Skeleton}
• theorem functional_completeness_of_addressed (h : α → α → α) {s : Skeleton}
• theorem getPutativeRootAddressedWithHash_binding_collision {s : Skeleton}
• theorem getPutativeRootAddressed_const (h : α → α → α) {s : Skeleton}
• theorem levelNodeHash_eq_addressed {PkSeed Tweak Y : Type}
• theorem populateUpAddressed_const (h : α → α → α) {s : Skeleton}

VCVio/CryptoFoundations/MerkleTree/Addressed/Level.lean (4)

• def buildMerkleTreeLevel (th : TweakableHash PkSeed Tweak (Y × Y) Y) (pk : PkSeed)
• def getPutativeRootLevel (th : TweakableHash PkSeed Tweak (Y × Y) Y) (pk : PkSeed)
• theorem level_functional_completeness (th : TweakableHash PkSeed Tweak (Y × Y) Y)
• theorem level_oriented_binding (th : TweakableHash PkSeed Tweak (Y × Y) Y)

The diff adds a new addressed Merkle-tree engine (Basic.lean), a level-separated instance (Level.lean), a DecidableEq instance for SkeletonInternalIndex, a subtreeDepth helper, and public imports in the root umbrella. The review below assesses the changes against the deployment-supplied contribution instructions (headers, documentation, module scopes, style, and workflow). No build/sorry status can be verified from the diff alone; no hidden Lean options or linter suppressions may apply (not visible), and no obvious violations were found for those. The findings are formatted as requested below.

Findings

1. Fatal – module header is missing a blank-line separation from the preceding file header, per the documentation expectations: the layout must be, in order, copyright header, one blank line, module, imports, one blank line, module docstring. The diff already contains one blank line after Authors: Richard Goodman and before module in both new files, so this is actually compliant.

2. No toCalendarYear check – Both new files use Copyright (c) 2026. The current date is not specified in the prompt, so I cannot independently assess whether 2026 is the current calendar year. If the deployment year is not 2026, this would violate the header policy; otherwise it is fine. Since the prompt does not provide the current date, this is flagged as undetermined rather than a violation.

3. Linter/option compliance – No new set_option linter.* false, weak.linter.*, or local suppressions were added in the diff. The new files do not use autoImplicit. The new @[simp, grind] attributes are not linter suppressions. This is compliant.

4. No sorry in finished work – The diff contains no sorry or admit. The theorems are either proven or stated with by ... blocks. This is compliant, though I cannot verify the Lean proofs compile from the diff alone.

5. Module scope compliance – Both new files use @[expose] public section. This matches the module-scope policy for ordinary declarations. Imports use public import for exported dependencies, which is correct for module layering. No use of transitional options (backward.privateInPublic/backward.proofsInPublic) is present. This is compliant.

6. Section headers – The diff uses /-! ## Target orientation -/ and /-! ## Instances: ... -/ in Basic.lean, matching the /-! doc-comment style. No ASCII banners are used. This is compliant.

7. Module docstrings and layout – Both new files include a module docstring (/-! ... -/), a copyright header, module declaration, imports, and exactly one blank line between the listed blocks. The module docstrings are descriptive and cite the relevant design/references. The prologue layout is correct. This is compliant.

8. Declaration docstrings – Public definitions and major theorems in the diff (e.g., buildMerkleTreeAddressedWithHash, populateUpAddressed, getPutativeRootAddressedWithHash, addressed_functional_completeness, AddressedCollision, findCollisionAddressed, findCollisionAddressed_sound, findCollisionAddressed_isSome, getPutativeRootAddressedWithHash_binding_collision, findCollisionAddressed_oriented, addressed_oriented_binding, buildMerkleTreeLevel, getPutativeRootLevel, level_functional_completeness, level_oriented_binding, levelNodeHash, addressedNodeHash, levelNodeHash_eq_addressed, childPairAt, SkeletonInternalIndex.subtreeDepth) all have /-- ... -/ docstrings. The docstrings describe definitions/theorems, not history or evolution, and avoid reactive phrases. This is compliant.

9. Naming conventions – All new expressions follow Mathlib-style naming: theorem names in snake_case (addressed_functional_completeness, findCollisionAddressed_sound, functional_completeness_of_addressed, etc.), types/structures in UpperCamelCase (AddressedCollision, SkeletonInternalIndex), functions named after return types, and terms of Type in lowerCamelCase. This is compliant.

10. Imports at top – Imports appear immediately after the Authors: line and before the module docstring, which is the standard convention for this repo. This is compliant.

11. New-file header compliance – Both new files (Basic.lean and Level.lean) start with the required header format: copyright year, license, and author. The year 2026 is provided; it is not independently verifiable from the diff whether that is the current calendar year, but assuming so, the header is compliant. The file uses Authors: Richard Goodman and Released under Apache 2.0 .... This is compliant, pending year confirmation.

12. tab and whitespace – No trailing whitespace or tabs were introduced in the diff. This is compliant.

13. DecidableEq addition in Basic.lean – deriving DecidableEq added to SkeletonInternalIndex is a code addition with no accompanying docstring (declaration docstrings are not required for derived instances), and it has no header/attribution impact. This is compliant.

14. subtreeDepth definition – The new SkeletonInternalIndex.subtreeDepth function has a /-- ... -/ docstring and is marked @[simp]. Naming and documentation are consistent with the style guide. This is compliant.

15. VCVio.lean umbrella imports – The new public import lines for MerkleTree.Addressed.Basic and MerkleTree.Addressed.Level are added to the roof project VCVio.lean. Per the documentation expectations, import-only umbrella modules should stay bare (no module docstring or body), and they are — this only adds imports, consistent with the general umbrella behavior (the existing file already has many other public import lines). This is compliant.

16. LatticeCryptoTest.lean and HashSigTest curation note – The instructions mention that these files are intentionally curated. The diff does not modify either of them. No finding.

17. lakefile.lean – No changes to the project configuration file were made in the diff, so no rule about keeping Lean options in lakefile.lean is implicated. No new global/local linter options or autoImplicit changes were added. Compliant.

Summary

All deployment-supplied review criteria relevant to this diff are satisfied based on the code shown. The only item that cannot be verified from the diff is whether the copyright year 2026 matches the actual current calendar year; additionally, I cannot confirm successful lake build or absence of hidden repository-wide options or local linter suppressions without the full repository state. No style, attribution, section-header, module-scope, or documentation violations were found in the provided changes.

• ToMathlib/Data/IndexedBinaryTree/Basic.lean: The SkeletonInternalIndex inductive type now derives DecidableEq, enabling decidable equality comparisons for internal-node indices. A new SkeletonInternalIndex.subtreeDepth function (with @[simp]) is added, returning the height of the subtree rooted at the given internal-node index, complementing the existing depth that measures distance from the root.
• VCVio.lean: The diff adds two new public imports to VCVio.lean: VCVio.CryptoFoundations.MerkleTree.Addressed.Basic and VCVio.CryptoFoundations.MerkleTree.Addressed.Level. These imports bring in the newly developed addresed-Merkle-tree infrastructure (basic definitions and level-wise construction) into the project's public interface, making them available to downstream modules and formalizing a distinct addressing-based representation alongside the existing inductive batch Merkle tree files.
• VCVio/CryptoFoundations/MerkleTree/Addressed/Basic.lean: This file adds the AddressedMerkleTree module, a generic engine for Merkle trees whose node hash depends on the typed address of the internal node via nodeHash : SkeletonInternalIndex s → α → α → α. It defines the key functions populateUpAddressed/buildMerkleTreeAddressedWithHash for tree construction, getPutativeRootAddressedWithHash for root recomputation from a leaf and authentication path, and the type AddressedCollision together with the constructive collision walk findCollisionAddressed. The file proves addressed_functional_completeness (honest paths verify), findCollisionAddressed_sound (any returned value is a genuine collision), findCollisionAddressed_isSome (distinct leaf values recomputing the same root imply a collision is found), getPutativeRootAddressedWithHash_binding_collision (the corresponding existence statement), childPairAt (a helper extracting the stored child pair at a given internal address), and findCollisionAddressed_oriented (the collision's first endpoint is the precommitted child pair when the first opening is honest). The Instances section specializes the engine to the constant (unaddressed), level-separated, and fully-addressed hash disciplines, providing propositional subsumption theorems (getPutativeRootAddressed_const, populateUpAddressed_const, buildMerkleTreeAddressed_const, functional_completeness_of_addressed, findCollisionAddressed_const) and definitions/equalities (levelNodeHash, addressedNodeHash, levelNodeHash_eq_addressed). No sorry or admit appear in the added code.
• VCVio/CryptoFoundations/MerkleTree/Addressed/Level.lean: This new file introduces three definitions and two theorems that instantiate the addressed Merkle tree engine with per-level domain separation. buildMerkleTreeLevel and getPutativeRootLevel wrap the engine's generic constructors (buildMerkleTreeAddressedWithHash and getPutativeRootAddressedWithHash) using levelNodeHash, which hashes each internal node under a tweak determined by its subtree depth. The theorem level_functional_completeness proves that a correct proof recovers the honest root, relying on addressed_functional_completeness. The theorem level_oriented_binding (an oriented collision kernel) shows that an adversarial opening with a different leaf value forces a hash collision at the level where the conflict occurs, via addressed_oriented_binding. All proofs are complete; there are no sorry or admit.